package derivable;

import static util.Validator.nonNull;

import java.util.Objects;

/**
 * @author Henrik Wall
 * @author Rudolf Schmidt
 * @author Eugen Nemirowski
 */
public final class Proposition implements Derivable<Proposition> {
	private final Operator op;
	private final boolean negated;
	private final Variable x;
	private final Variable y;

	private Proposition(final Operator op, final boolean negated, final Variable x, final Variable y) {
		this.op = op;
		this.negated = negated;
		this.x = x;
		this.y = y;
	}

	/**
	 * Creates a new {@link Proposition}.
	 * 
	 * @param op the operator (non-null)
	 * @param negated if the proposition is negated
	 * @param x first variable (non-null)
	 * @param y second variable
	 * @return a new {@link Proposition}
	 */
	public static Proposition create(final Operator op, final boolean negated, final Variable x, final Variable y) {
		return new Proposition(nonNull(op, "op must not be null"), negated, nonNull(x, "x must not be null"), y);
	}

	/**
	 * Creates a new {@link Proposition}.
	 * 
	 * @param op the operator (non-null)
	 * @param negated if the proposition is negated
	 * @param x first variable (non-null)
	 * @return a new {@link Proposition}
	 * @see Proposition#create(Operator, boolean, Variable, Variable)
	 */
	public static Proposition create(final Operator op, final boolean negated, final Variable x) {
		return create(op, negated, x, null);
	}

	/**
	 * For {@link Proposition}s p, p': derives(p, p'): <=> p.equals(p')
	 */
	@Override
	public boolean derives(final Proposition o) {
		return equals(o);
	}

	public Operator getOp() {
		return op;
	}

	public boolean isNegated() {
		return negated;
	}

	public Variable getX() {
		return x;
	}

	public Variable getY() {
		return y;
	}

	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + (negated ? 1231 : 1237);
		result = prime * result + op.hashCode();
		return result;
	}

	@Override
	public boolean equals(final Object obj) {
		if (this == obj) {
			return true;
		}
		if (obj == null) {
			return false;
		}
		if (getClass() != obj.getClass()) {
			return false;
		}
		final Proposition other = (Proposition) obj;
		if (negated != other.negated) {
			return false;
		}
		if (op != other.op) {
			return false;
		}
		if (!x.equals(other.x)) {
			if (!op.isSymmetric()) {
				return false;
			}
			return x.equals(other.y) && other.x.equals(y);
		}
		return Objects.equals(y, other.y);
	}

	@Override
	public String toString() {
		return (negated ? "!" : "") + "(" + x + op + y + ")";
	}
}